(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const _21-0 (_ BitVec 21))
(assert (forall ((q0 Bool) (q1 (_ BitVec 21))) v5))
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(push)
(declare-const v12 Bool)
(push)
(declare-const v13 Bool)
(assert (exists ((q2 Bool) (q3 Bool) (q4 Bool) (q5 (_ BitVec 1))) v7))
(pop)
(declare-const v14 Bool)
(assert (or v7 (= _21-0 _21-0 _21-0 (bvxor _21-0 _21-0) _21-0) v3))
(assert (or v14 v7 v4))
(assert (or v14 v6 (= _21-0 _21-0 _21-0 (bvxor _21-0 _21-0) _21-0)))
(assert (or v14 v10 v10))
(assert (or (= _21-0 _21-0 _21-0 (bvxor _21-0 _21-0) _21-0) v4 (= _21-0 _21-0 _21-0 (bvxor _21-0 _21-0) _21-0)))
(assert (or (= (bvxor _21-0 _21-0) (bvudiv _21-0 (bvxor _21-0 (bvmul _21-0 (bvxor _21-0 _21-0)))) (bvxor _21-0 _21-0) (bvmul _21-0 (bvxor _21-0 _21-0))) v8 (= (bvxor _21-0 _21-0) (bvudiv _21-0 (bvxor _21-0 (bvmul _21-0 (bvxor _21-0 _21-0)))) (bvxor _21-0 _21-0) (bvmul _21-0 (bvxor _21-0 _21-0)))))
(assert (or (bvslt (bvxor _21-0 _21-0) (bvmul _21-0 (bvxor _21-0 _21-0))) (= v3 v4 v5 v8 v6 v2) v14))
(check-sat)
